# Abstract

Advances & challenges in model-based deductive verification of programs

This talk encompasses two subjects of my PhD. First, we present "Verified JavaBIP", a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machines, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. We address this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the "Solidity Casino" case study, known from the VerifyThis Collaborative Long Term Challenge.

Second, in a previous PhD thesis Wytse Oortwijn presented "An Abstraction Technique for Describing Concurrent Program Behaviour". This technique requires specifying program behaviour as an abstract process-algebraic model. Then, by proving that a program follows the model, properties proven over the model can be assumed for (deductive) verification of the program. The technique has been successfully applied to verifying an implementation of the distributed leader election algorithm. As the current form of this technique has some limitations, we would like to discuss what other challenges we can apply this technique to. Specifically, we will be discussing what we mean by "interesting" properties: those that are both easy to check with a model checker, and meaningful in a program verification context.